Inference at * 2 2 
Iof proof for Lemma member-zip:



1. A : Type
2. B : Type
3. A List
4. u : A
5. v : A List
6. ys:(B List), x:A, y:B. (<x, y>  zip(v;ys))  {(x  v) & (y  ys)}
7. B List
8. u1 : B
9. v1 : B List
10. x:A, y:B. (<x, y>  zip([u / v];v1))  {(x  [u / v]) & (y  v1)}
  x:A, y:B. (<x, y>  zip([u / v];[u1 / v1]))  {(x  [u / v]) & (y  [u1 / v1])} 

latex

 by Reduce 0 THEN Auto THEN RWO "cons_member" (-1) THENA Auto 
THEN D (-1) 

latex

TH1: 

TH1: 11. x : A
TH1: 12. y : B
TH1: 13. <x, y> = <u, u1>
TH1:   {(x  [u / v]) & (y  [u1 / v1])}
TH2: 

TH2: 11. x : A
TH2: 12. y : B
TH2: 13. (<x, y>  zip(v;v1))
TH2:   {(x  [u / v]) & (y  [u1 / v1])}
TH.

Definitions	{T}, (x  l), [car / cdr], P  Q, P & Q, P  Q, x:AB(x), x:A  B(x), zip(as;bs), x:A. B(x), <a, b>, t  T, P  Q, left + right
Lemmas	l member wf, cons member, zip wf